package arlab.formulae.tests
import arlab.formulae._
import arlab.formulae.transformations._



object Blatt4 {
    def main (args: Array[String]) ={
    
        val a = And(Or(BooleanVariable("p"), 
                       And(BooleanVariable("q"), 
                           Not(BooleanVariable("r")))),
                    BooleanVariable("s")) 
        println("normal:")
        println(a)
        println("tseit:")
        println(Transformations.tseitincnf2(a))
    
        
        val b = Predicate("P",Function ("f",Variable("a"), Variable("b"), Variable("a")))
        println("normal:")
        println(b)
        println("generalized:")
        println(Transformations.generalize(b))
        
        
        val c2 = Or(Or(Or(Or(And(BooleanVariable("a"),BooleanVariable("b")),
                            BooleanVariable("c")),
                         BooleanVariable("d")),
                      BooleanVariable("e")),
                   BooleanVariable("f"))
        println("normal:")
        println(c2)           
        println("tseitincnf:")
        println(Transformations.tseitincnf2(c2))
        

        val h = And(Or(Or(Or(Or(BooleanVariable("a"),BooleanVariable("b")),
                            BooleanVariable("c")),
                         BooleanVariable("d")),
                      BooleanVariable("e")),
                   BooleanVariable("f"))  
        println("normal:")
        println(h)           
        println("tseitincnf:")
        println(Transformations.tseitincnf2(h))      
        
        val d2 = Or(And(BooleanVariable("a"),BooleanVariable("b")),BooleanVariable("c"))
        println("normal:")
        println(d2)           
        println("tseitincnf:")
        println(Transformations.tseitincnf2(d2))
    

        val c = ForAll(Variable("a"), Exists(Variable ("b"), Predicate("P",Function ("f",Variable("a"), Variable("b"), Variable("a")))))
        println("normal:")
        println(c)
        println("matrix:")
        println(Transformations.matrix(c))

        val d = Predicate("P",Variable("x"))&&(ForAll(Variable("x"),Predicate("Q",Variable("x"))||(Predicate("R",Variable("y"))&&(Exists(Variable("y"),Predicate("P",Variable("y")))))))
        println("normal:")
        println(d)
        println("matrix:")
        println(Transformations.matrix(d))

        val e = Predicate("P",Variable("x"))&&(ForAll(Variable("x"),Predicate("Q",Variable("x"))||(Predicate("R",Variable("y"))&&(ForAll(Variable("y"),Predicate("P",Variable("y")))))))
        println("normal:")
        println(e)
        println("matrix:")
        println(Transformations.matrix(e))
      
      
        val f = Or(Or(Predicate ("P", Variable("a")), Predicate ("Q", Variable("b"))), Predicate ("R", Variable("c")))
        println("normal:")
        println(f)
        println("createClause:")
        println(ClauseSet.create(f))

        val g = And(And(Predicate ("P", Variable("a")), Predicate ("Q", Variable("b"))), Predicate ("R", Variable("c")))
        println("normal:")
        println(g)
        println("createClause:")
        println(ClauseSet.create(g))
        
        
        val j = List((Variable("a"), Variable("b")),(Variable("b"),Variable("c")),(Variable("c"), Variable("a")))
        println("normal:")
        println(j)
        println("unifiable?, expects true")
        println(Unification.unifiable(j))
        
        val l = List((Function("f", Variable ("b")), Variable("c")), (Function("f", Variable ("d")), Function("g", Variable("a"))))
        println("normal:")
        println(l)
        println("unifiable?, expects false")
        println(Unification.unifiable(l))

        val i = List((Function("f", Variable ("x")),(Function("f", Variable ("x")))), (Function("f", Variable ("x")),(Function("f", Variable ("y")))))
        println("normal:")
        println(i)
        println("unify:")
        println(Unification.unifiable(i))

        val k = List((Function("f", Variable ("x")),(Function("f", Variable ("x")))), (Function("g", Variable ("x")),(Function("f", Variable ("y")))))
        println("normal:")
        println(k)
        println("unify:")
        println(Unification.unifiable(k))

        val m = List((Function("f",Variable("x"), Function("h",Variable ("y"))),(Function("f",Function("g", Variable ("a")),Variable("z")))),(Variable ("z"),(Function("h", Variable ("y")))),(Variable("w"),Variable("z")))
        println("normal:")
        println(m)
        println("unify:")
        println(Unification.unifiable(m))

        //geht noch nicht muss False ausgeben!!!! // GEHT JA WOHL
        val n = List((Function("f", Variable ("x")),Variable("x")))
        println("normal:")
        println(n)
        println("unify:")
        println(Unification.unifiable(n))
        
        val o = List((Predicate("a"), Predicate("b")),(Predicate("b"),Predicate("c")),(Predicate("c"), Predicate("a"))) 
        println("normal:")
        println(o)
        println("unify, expects false")
        println(Unification.unifyPredicate(o))
        
        val p = List((Predicate("P",Variable("a"),Variable("b"),Variable("c") ), 
                      Predicate("P",Variable("b"),Variable("c"),Variable("a"))))
        println("normal:")
        println(p)
        println("unify, expects true")
        println(Unification.unifyPredicate(p))
    }
}
